$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), ${\it eq}$:EqDecider($A$), $f$, $g$:$a$:$A$ fp$\rightarrow$ $B$($a$), $x$:$A$, $P$:($a$:$A$$\rightarrow$$B$($a$)$\rightarrow\mathbb{P}$).
\\[0ex]$g$ $\subseteq$ $f$ $\Rightarrow$ ($z$ != $f$($x$) $\Rightarrow$ $P$($x$,$z$)) $\Rightarrow$ ($z$ != $g$($x$) $\Rightarrow$ $P$($x$,$z$))